\section{Implementation Ideas}

\subsection{Input}
The FD solver accepts as input a tuple of the following:
\begin{itemize}
	\item \textbf{a list of free variables} whose value it must
	determine
	\item \textbf{a type-checked Scala program} \textit{(optional)} during the
	type-checking of which the type of the above mentioned free variables was
	inferred.
	\item \textbf{a list of constraints} well-typed Scala expressions, returning a
	Boolean value.
\end{itemize}

\subsection{Pre-treatment}
First of all, the ``Program'' part of the input should be converted to Single
Static Assignment form and from there converted into constraints.

Then the Constraint set should be adapted so that for
each variable $v$ appearing in a Constraint $c$, a new constraint $c_v$ of the
form $v$ 
BinOp Expr is present in the new Constraint set

\subsection{Range}
Ranges in our implementation are defined similarly as in the GNU-Prolog compiler integrated FD solver, however, they
are not restricted to integer values and can be expanded to any partially
ordered data. Therefore they have a type parameter,
called ``valuesType''. A range is represented by a \textit{min} and a \textit{max} element, and contains any
element $e$ of the domain such that $min \leq e \land e \leq max$. The default range of a value is :
\begin{lstlisting}
	def defaultRange = Range[valuesType] {
		def min = getMin(valuesType)
		def max = getMax(valuesType)
	}
\end{lstlisting}
Another limitation of the GNU-Prolog FD Solver is that whenever the possible values for a variable are not continuous,
it stores them in a vector rather than a range, with a limited vector size, and therefore might lose interesting
values. To avoid this issue, \textit{MultiRanges} can be used.

\subsection{MultiRange}
A \textit{MultiRange} is a list of \textit{Ranges} including some helper methods. It should notably be able to:
\begin{itemize}
	\item compute its intersection with another \textit{MultiRange} of the same type. This is for constraints of type $a
= b$, which restrict the possible values for each $a$ and $b$ to the intersection of their previous possible values
sets.
	\item update its value according to a constraint. For instance $x \geq 2$ excludes all values $< 2$.
	\item yield a new \textit{MultiRange} mapped to any operation valid on its ``valuesType''. This is to be used when a
constraint compares a variable to the result of an operation, as in $x \leq y - 32$. In this case, the
\textit{MultiRange} of $x$ would be updated to the intersection of its previous \textit{MultiRange} with that of the
MultiRange of y mapped to $\{\_ - 32\}$ (\textit{ie. } every range border value
is decreased by 32).
\end{itemize}
Clearly this implies that a new \textit{MultiRange} subtype must be defined for every new domain in which variables can
take their values. Furthermore, for some specific constraints, it requires more
space than GNU-Prolog's vector based approach (notably $x\ \%\ 2 = 0$). However,
it should perform better on average.

\subsection{ExtDPLL}
Putting most of the abstraction load onto the \textit{MultiRange} implementation allows for a clearer a simpler
extension of DPLL than would have been otherwise possible. Recall the original definition of DPLL, as seen in class:
\begin{lstlisting}
def DPLL(S : Set[Clause]) : boolean =
  val S' = RemoveSubsumed(BCP(S))
  if (emptyClause in S') then false
  else if (S' has only unit clauses) then true
  else
     val P = pick variable from FV(S')
     DPLL(F' union {p}) or DPLL(F' union {Not(p)})
\end{lstlisting}
Adapting it to the suggested implementation yields the following result
\begin{lstlisting}
def ExtDPLL(cs: List/Set[Constraint], mrs: HashMap[FreeVar, MultiRange]): Option[Solution] = {
  val (cstmp, mrs1) = ECP(cs, mrs)
  val cs1 = RemoveSubsumed(cstmp, mrs)
  if (empty MultiRange in mrs1) then None
  else if (all constraints are satified) then Some(mrs1)
  else {
    val v: pick free variable in mrs1.keys
    ExtDPLL(cs1, mrs1.update(v -> lowerVals(v))) match {
      case Some(sol) => Some(sol)
      case None => ExtDPLL(cs1, mrs1.update(v -> upperVals(v)))
    }
  }
\end{lstlisting}



\subsection{ECP}
ECP stands for Extended Constraint Propagation. Its implementation is based on
the assumption that constraints have been properly type-checked and makes use of
the MultiRange specialized functions mentioned earlier. It consists of
alternated steps of proper ``Constraint propagation'' and MultiRange updating
steps. 
